COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 00003	c(xx,mem) - The contents off the location xx when the memory state is mem.
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.at "qgo" ⊂"%3go_to%*"⊃
.at "qbegin" ⊂"%3begin%*"⊃
.at "end" ⊂"%endn%*"⊃
.at "end" ⊂"%endn%*"⊃
.cb Correctness of Programs that Modify List Structure

	Consider the LISP program ⊗nconc defined by

.begin nofill

nconc[u,v] ← qif qn u qthen v
		qelse prog[[w]
	w ← u
l:	qif qn qd w qthen qbegin jnk ← rplacd[w,v]; return u qend;
	w ← qd w
	qgo l]
.end

	⊗nconc is a destructive version of ⊗append in that a variable
whose value is ⊗u is changed to have value ⊗u*v.
Other variables are unchanged if they don't merge with the top
level of ⊗u.  How shall we state this formally and prove it?

	We begin by distinguishing between S-expressions and
pointers and by introducing the memory state ⊗mem and
the function ⊗val(uu,m).  We shall use single letters for variables
whose values are S-expressions and doubled letters for variables whose
values are pointers.  A typical relation might be

	%2val(xx,mem) = x%1

meaning that the pointer ⊗xx points to a list structure representing
the S-expression which is the value of the S-expression variable
⊗x.  

	We now introduce ⊗nconc(xx,_vv,_mem) as a two output function
whose value is a new pointer and a new memory state.  We shall
want to prove

	%2∀uu mem. val(nconc(uu, vv, mem) = val(uu, mem) * val(vv, mem)%1

as the relation between ⊗nconc and ⊗append. 
However, this isn't all we will need to prove about ⊗nconc. 

	The program can now be written cleanly as

.begin nofill

%2nconc[uu, vv, mem] ← qif null[uu, mem] qthen vv, mem
			qelse prog[[ww, jjnk]
	ww ← uu;
l:	qif null cdr[ww, mem] qthen 
		qbegin jjnk, mem ← rplacd[ww, vv, mem] return2[uu, mem] qend;
	ww ← cdr[ww, mem];
	qgo l]%1.
.end

	Perhaps we should now try to elephantize the program, but it
still isn't clear how to elephantize function calls.

c(xx,mem) - The contents off the location xx when the memory state is mem.

issexp(xx,mem) - True if  xx points to a list structure representing an
S-expression

sexp(xx,mem) - The S-expression represented by the pointer xx in mem.

satom(xx,mem) - True if xx points to an atom.

atomrep(xx,mem) - The atom pointed to by xx.

	We have the axiom

	∀xx mem.[satom(xx,mem) ⊃ atom atomrep(xx,mem)],

which asserts that a when a pointer satisfies the test for an atom,
the function atomrep returns an atom.

	With these we can make the recursive definition

	sexp(xx,mem) ← if satom(xx,mem) then atomrep(xx,mem)
else sexp(left c(xx,mem),mem).sexp(right c(xx,mem),mem).